$\forall$${\it es}$:ES, $T$:Type, $X$:MaInterface($T$), $i$:Id.
\\[0ex]($\uparrow$$i$ $\in$ dom($X$)) $\Rightarrow$ (ma{-}interface{-}consistent{-}at(${\it es}$;$i$;$X$) $\in$ $\mathbb{P}$)